Step of Proof: or_functionality_wrt_iff 9,38
Inference at * 2 
Iof proof for Lemma or functionality wrt iff:



1. P1 : 
2. P2 : 
3. Q1 : 
4. Q2 : 
5. P1  P2
6. Q1  Q2
7. P2  Q2
  P1  Q1 
latex
 by ((((D 7 THENL [Sel 1 (D 0);Sel 2 (D 0)]) 
CollapseTHENM (HypBackchain))) 
CollapseTHENA (
C(Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 4:n)) (first_tok :t) inil_term))) 
latex

C.

Definitionst  T, P  Q, P  Q, P  Q, P  Q, P  Q,

origin